Inference at * 
Iof proof for Lemma branch-ifthenelse:


  b:, P, Q:Top. if x:b then P else Q fi  ~ if b then P else Q fi  

latex

 by ((UnivCD) 
CollapseTHENA (Auto)) 

latex

Co1: 

Co1: 1. b : 
Co1: 2. P : Top
Co1: 3. Q : Top
Co1:   if x:b then P else Q fi  ~ if b then P else Q fi 
Co.

Definitions	x:A. B(x), Top, t  T,
Lemmas	top wf, bool wf